

LEMMA

If x is a tangential proper part of y and y partially overlaps z, then z is not part of x.
=============================
Step 1

? (all x (all y (all z (((tpp x y) & (po y z)) => (~ (p z x))))))


> revsk
=============================
Step 2

? (((~ (tpp c1274190 c1274189)) v (~ (po c1274189 c1274188))) v (~ (p c1274188 c1274190)))


> hypdisj
=============================
Step 3

? (~ (p c1274188 c1274190))

1. (po c1274189 c1274188)
2. (tpp c1274190 c1274189)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 4
|
|? (c (f1269137 c1274188 Var47 Var48) c1274188)
|
|1. (p c1274188 c1274190)
|2. (po c1274189 c1274188)
|3. (tpp c1274190 c1274189)
|
|> ((c (f1269137 Y Z X) Y) <-- (~ (p Y Z)))
|=============================
|Step 5
|
|? (~ (p c1274188 Var47))
|
|1. (~ (c (f1269137 c1274188 Var47 Var48) c1274188))
|2. (p c1274188 c1274190)
|3. (po c1274189 c1274188)
|4. (tpp c1274190 c1274189)
|
|> ((~ (p Y X)) <-- (po X Y))
|=============================
|Step 6
|
|? (po Var47 c1274188)
|
|1. (p c1274188 Var47)
|2. (~ (c (f1269137 c1274188 Var47 Var48) c1274188))
|3. (p c1274188 c1274190)
|4. (po c1274189 c1274188)
|5. (tpp c1274190 c1274189)
|
|> hyp
=============================
Step 7

? (~ (c (f1269137 c1274188 c1274189 Var48) c1274190))

1. (p c1274188 c1274190)
2. (po c1274189 c1274188)
3. (tpp c1274190 c1274189)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 8
|
|? (p c1274190 Var54)
|
|1. (c (f1269137 c1274188 c1274189 Var48) c1274190)
|2. (p c1274188 c1274190)
|3. (po c1274189 c1274188)
|4. (tpp c1274190 c1274189)
|
|> ((p X Y) <-- (pp X Y))
|=============================
|Step 9
|
|? (pp c1274190 Var54)
|
|1. (~ (p c1274190 Var54))
|2. (c (f1269137 c1274188 c1274189 Var48) c1274190)
|3. (p c1274188 c1274190)
|4. (po c1274189 c1274188)
|5. (tpp c1274190 c1274189)
|
|> ((pp X Y) <-- (tpp X Y))
|=============================
|Step 10
|
|? (tpp c1274190 Var54)
|
|1. (~ (pp c1274190 Var54))
|2. (~ (p c1274190 Var54))
|3. (c (f1269137 c1274188 c1274189 Var48) c1274190)
|4. (p c1274188 c1274190)
|5. (po c1274189 c1274188)
|6. (tpp c1274190 c1274189)
|
|> hyp
=============================
Step 11

? (~ (c (f1269137 c1274188 c1274189 Var48) c1274189))

1. (c (f1269137 c1274188 c1274189 Var48) c1274190)
2. (p c1274188 c1274190)
3. (po c1274189 c1274188)
4. (tpp c1274190 c1274189)

> ((~ (c (f1269137 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 12

? (~ (p c1274188 c1274189))

1. (c (f1269137 c1274188 c1274189 Var48) c1274189)
2. (c (f1269137 c1274188 c1274189 Var48) c1274190)
3. (p c1274188 c1274190)
4. (po c1274189 c1274188)
5. (tpp c1274190 c1274189)

> ((~ (p Y X)) <-- (po X Y))
=============================
Step 13

? (po c1274189 c1274188)

1. (p c1274188 c1274189)
2. (c (f1269137 c1274188 c1274189 Var48) c1274189)
3. (c (f1269137 c1274188 c1274189 Var48) c1274190)
4. (p c1274188 c1274190)
5. (po c1274189 c1274188)
6. (tpp c1274190 c1274189)

> hyp


LEMMA

Tangential proper part implies proper part.
=============================
Step 1

? (all x (all y ((tpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (tpp c1279419 c1279418)) v (pp c1279419 c1279418))


> hypdisj
=============================
Step 3

? (pp c1279419 c1279418)

1. (tpp c1279419 c1279418)

> ((pp X Y) <-- (tpp X Y))
=============================
Step 4

? (tpp c1279419 c1279418)

1. (~ (pp c1279419 c1279418))
2. (tpp c1279419 c1279418)

> hyp


LEMMA

Proper part implies parthood.
=============================
Step 1

? (all x (all y ((pp x y) => (p x y))))


> revsk
=============================
Step 2

? ((~ (pp c1284704 c1284703)) v (p c1284704 c1284703))


> hypdisj
=============================
Step 3

? (p c1284704 c1284703)

1. (pp c1284704 c1284703)

> ((p X Y) <-- (pp X Y))
=============================
Step 4

? (pp c1284704 c1284703)

1. (~ (p c1284704 c1284703))
2. (pp c1284704 c1284703)

> hyp


LEMMA

Partial overlap implies overlap.
=============================
Step 1

? (all x (all y ((po x y) => (o x y))))


> revsk
=============================
Step 2

? ((~ (po c1290045 c1290044)) v (o c1290045 c1290044))


> hypdisj
=============================
Step 3

? (o c1290045 c1290044)

1. (po c1290045 c1290044)

> ((o X Y) <-- (po X Y))
=============================
Step 4

? (po c1290045 c1290044)

1. (~ (o c1290045 c1290044))
2. (po c1290045 c1290044)

> hyp


LEMMA

Overlap implies connection.
=============================
Step 1

? (all x (all y ((o x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (o c1295442 c1295441)) v (c c1295442 c1295441))


> hypdisj
=============================
Step 3

? (c c1295442 c1295441)

1. (o c1295442 c1295441)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var48 c1295441)
|
|1. (~ (c c1295442 c1295441))
|2. (o c1295442 c1295441)
|
|> ((p Z X) <-- (~ (c (f1290085 Z X Y) Z)))
|=============================
|Step 5
|
|? (~ (c (f1290085 Var48 c1295441 Var51) Var48))
|
|1. (~ (p Var48 c1295441))
|2. (~ (c c1295442 c1295441))
|3. (o c1295442 c1295441)
|
|> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
||=============================
||Step 6
||
||? (p (f1290102 Var57 Var54) Var54)
||
||1. (c (f1290085 (f1290102 Var57 Var54) c1295441 Var51) (f1290102 Var57 Var54))
||2. (~ (p (f1290102 Var57 Var54) c1295441))
||3. (~ (c c1295442 c1295441))
||4. (o c1295442 c1295441)
||
||> ((p (f1290102 X Y) Y) <-- (o X Y))
||=============================
||Step 7
||
||? (o Var57 Var54)
||
||1. (~ (p (f1290102 Var57 Var54) Var54))
||2. (c (f1290085 (f1290102 Var57 Var54) c1295441 Var51) (f1290102 Var57 Var54))
||3. (~ (p (f1290102 Var57 Var54) c1295441))
||4. (~ (c c1295442 c1295441))
||5. (o c1295442 c1295441)
||
||> hyp
|=============================
|Step 8
|
|? (~ (c (f1290085 (f1290102 c1295442 c1295441) c1295441 Var51) c1295441))
|
|1. (c (f1290085 (f1290102 c1295442 c1295441) c1295441 Var51) (f1290102 c1295442 c1295441))
|2. (~ (p (f1290102 c1295442 c1295441) c1295441))
|3. (~ (c c1295442 c1295441))
|4. (o c1295442 c1295441)
|
|> ((~ (c (f1290085 Y Z X) Z)) <-- (~ (p Y Z)))
|=============================
|Step 9
|
|? (~ (p (f1290102 c1295442 c1295441) c1295441))
|
|1. (c (f1290085 (f1290102 c1295442 c1295441) c1295441 Var51) c1295441)
|2. (c (f1290085 (f1290102 c1295442 c1295441) c1295441 Var51) (f1290102 c1295442 c1295441))
|3. (~ (p (f1290102 c1295442 c1295441) c1295441))
|4. (~ (c c1295442 c1295441))
|5. (o c1295442 c1295441)
|
|> hyp
=============================
Step 10

? (c c1295442 (f1290102 c1295442 c1295441))

1. (~ (c c1295442 c1295441))
2. (o c1295442 c1295441)

> ((c Y X) <-- (c X Y))
=============================
Step 11

? (c (f1290102 c1295442 c1295441) c1295442)

1. (~ (c c1295442 (f1290102 c1295442 c1295441)))
2. (~ (c c1295442 c1295441))
3. (o c1295442 c1295441)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 12
|
|? (p (f1290102 c1295442 Var71) c1295442)
|
|1. (~ (c (f1290102 c1295442 c1295441) c1295442))
|2. (~ (c c1295442 (f1290102 c1295442 c1295441)))
|3. (~ (c c1295442 c1295441))
|4. (o c1295442 c1295441)
|
|> ((p (f1290102 X Y) X) <-- (o X Y))
|=============================
|Step 13
|
|? (o c1295442 Var71)
|
|1. (~ (p (f1290102 c1295442 Var71) c1295442))
|2. (~ (c (f1290102 c1295442 c1295441) c1295442))
|3. (~ (c c1295442 (f1290102 c1295442 c1295441)))
|4. (~ (c c1295442 c1295441))
|5. (o c1295442 c1295441)
|
|> hyp
=============================
Step 14

? (c (f1290102 c1295442 c1295441) (f1290102 c1295442 c1295441))

1. (~ (c (f1290102 c1295442 c1295441) c1295442))
2. (~ (c c1295442 (f1290102 c1295442 c1295441)))
3. (~ (c c1295442 c1295441))
4. (o c1295442 c1295441)

> ((c X X) <--)


LEMMA

Parthood transports connection from part to whole.
=============================
Step 1

? (all x (all y (all z (((p x y) & (c z x)) => (c z y)))))


> revsk
=============================
Step 2

? (((~ (p c1300897 c1300896)) v (~ (c c1300895 c1300897))) v (c c1300895 c1300896))


> hypdisj
=============================
Step 3

? (c c1300895 c1300896)

1. (c c1300895 c1300897)
2. (p c1300897 c1300896)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var24 c1300896)
|
|1. (~ (c c1300895 c1300896))
|2. (c c1300895 c1300897)
|3. (p c1300897 c1300896)
|
|> hyp
=============================
Step 5

? (c c1300895 c1300897)

1. (~ (c c1300895 c1300896))
2. (c c1300895 c1300897)
3. (p c1300897 c1300896)

> hyp


LEMMA

Split x,z into disconnection or connection.
=============================
Step 1

? (all x (all y (all z (((tpp x y) & (po y z)) => ((dc x z) v (c x z))))))


> revsk
=============================
Step 2

? (((~ (tpp c1306508 c1306507)) v (~ (po c1306507 c1306506))) v ((dc c1306508 c1306506) v (c c1306508 c1306506)))


> hypdisj
=============================
Step 3

? (c c1306508 c1306506)

1. (~ (dc c1306508 c1306506))
2. (po c1306507 c1306506)
3. (tpp c1306508 c1306507)

> ((c X Y) <-- (~ (dc X Y)))
=============================
Step 4

? (~ (dc c1306508 c1306506))

1. (~ (c c1306508 c1306506))
2. (~ (dc c1306508 c1306506))
3. (po c1306507 c1306506)
4. (tpp c1306508 c1306507)

> hyp


LEMMA

In the connected case, classify x,z as ec or po or pp.
=============================
Step 1

? (all x (all y (all z ((((tpp x y) & (po y z)) & (c x z)) => ((ec x z) v ((po x z) v (pp x z)))))))


> revsk
=============================
Step 2

? ((((~ (tpp c1312385 c1312384)) v (~ (po c1312384 c1312383))) v (~ (c c1312385 c1312383))) v ((ec c1312385 c1312383) v ((po c1312385 c1312383) v (pp c1312385 c1312383))))


> hypdisj
=============================
Step 3

? (pp c1312385 c1312383)

1. (~ (po c1312385 c1312383))
2. (~ (ec c1312385 c1312383))
3. (c c1312385 c1312383)
4. (po c1312384 c1312383)
5. (tpp c1312385 c1312384)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 4
|
|? (p c1312385 c1312383)
|
|1. (~ (pp c1312385 c1312383))
|2. (~ (po c1312385 c1312383))
|3. (~ (ec c1312385 c1312383))
|4. (c c1312385 c1312383)
|5. (po c1312384 c1312383)
|6. (tpp c1312385 c1312384)
|
|> ((p X Y) <-- (o X Y) (~ (p Y X)) (~ (po X Y)))
|||=============================
|||Step 5
|||
|||? (o c1312385 c1312383)
|||
|||1. (~ (p c1312385 c1312383))
|||2. (~ (pp c1312385 c1312383))
|||3. (~ (po c1312385 c1312383))
|||4. (~ (ec c1312385 c1312383))
|||5. (c c1312385 c1312383)
|||6. (po c1312384 c1312383)
|||7. (tpp c1312385 c1312384)
|||
|||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
||||=============================
||||Step 6
||||
||||? (c c1312385 c1312383)
||||
||||1. (~ (o c1312385 c1312383))
||||2. (~ (p c1312385 c1312383))
||||3. (~ (pp c1312385 c1312383))
||||4. (~ (po c1312385 c1312383))
||||5. (~ (ec c1312385 c1312383))
||||6. (c c1312385 c1312383)
||||7. (po c1312384 c1312383)
||||8. (tpp c1312385 c1312384)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (~ (ec c1312385 c1312383))
|||
|||1. (~ (o c1312385 c1312383))
|||2. (~ (p c1312385 c1312383))
|||3. (~ (pp c1312385 c1312383))
|||4. (~ (po c1312385 c1312383))
|||5. (~ (ec c1312385 c1312383))
|||6. (c c1312385 c1312383)
|||7. (po c1312384 c1312383)
|||8. (tpp c1312385 c1312384)
|||
|||> hyp
||=============================
||Step 8
||
||? (~ (p c1312383 c1312385))
||
||1. (~ (p c1312385 c1312383))
||2. (~ (pp c1312385 c1312383))
||3. (~ (po c1312385 c1312383))
||4. (~ (ec c1312385 c1312383))
||5. (c c1312385 c1312383)
||6. (po c1312384 c1312383)
||7. (tpp c1312385 c1312384)
||
||> ((~ (p Z X)) <-- (tpp X Y) (po Y Z))
|||=============================
|||Step 9
|||
|||? (tpp c1312385 Var46)
|||
|||1. (p c1312383 c1312385)
|||2. (~ (p c1312385 c1312383))
|||3. (~ (pp c1312385 c1312383))
|||4. (~ (po c1312385 c1312383))
|||5. (~ (ec c1312385 c1312383))
|||6. (c c1312385 c1312383)
|||7. (po c1312384 c1312383)
|||8. (tpp c1312385 c1312384)
|||
|||> hyp
||=============================
||Step 10
||
||? (po c1312384 c1312383)
||
||1. (p c1312383 c1312385)
||2. (~ (p c1312385 c1312383))
||3. (~ (pp c1312385 c1312383))
||4. (~ (po c1312385 c1312383))
||5. (~ (ec c1312385 c1312383))
||6. (c c1312385 c1312383)
||7. (po c1312384 c1312383)
||8. (tpp c1312385 c1312384)
||
||> hyp
|=============================
|Step 11
|
|? (~ (po c1312385 c1312383))
|
|1. (~ (p c1312385 c1312383))
|2. (~ (pp c1312385 c1312383))
|3. (~ (po c1312385 c1312383))
|4. (~ (ec c1312385 c1312383))
|5. (c c1312385 c1312383)
|6. (po c1312384 c1312383)
|7. (tpp c1312385 c1312384)
|
|> hyp
=============================
Step 12

? (~ (p c1312383 c1312385))

1. (~ (pp c1312385 c1312383))
2. (~ (po c1312385 c1312383))
3. (~ (ec c1312385 c1312383))
4. (c c1312385 c1312383)
5. (po c1312384 c1312383)
6. (tpp c1312385 c1312384)

> ((~ (p Z X)) <-- (tpp X Y) (po Y Z))
|=============================
|Step 13
|
|? (tpp c1312385 Var52)
|
|1. (p c1312383 c1312385)
|2. (~ (pp c1312385 c1312383))
|3. (~ (po c1312385 c1312383))
|4. (~ (ec c1312385 c1312383))
|5. (c c1312385 c1312383)
|6. (po c1312384 c1312383)
|7. (tpp c1312385 c1312384)
|
|> hyp
=============================
Step 14

? (po c1312384 c1312383)

1. (p c1312383 c1312385)
2. (~ (pp c1312385 c1312383))
3. (~ (po c1312385 c1312383))
4. (~ (ec c1312385 c1312383))
5. (c c1312385 c1312383)
6. (po c1312384 c1312383)
7. (tpp c1312385 c1312384)

> hyp


LEMMA

Proper part splits into tangential or non-tangential proper part.
=============================
Step 1

? (all x (all y ((pp x y) => ((tpp x y) v (ntpp x y)))))


> revsk
=============================
Step 2

? ((~ (pp c1318872 c1318871)) v ((tpp c1318872 c1318871) v (ntpp c1318872 c1318871)))


> hypdisj
=============================
Step 3

? (ntpp c1318872 c1318871)

1. (~ (tpp c1318872 c1318871))
2. (pp c1318872 c1318871)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f1312496 Z X Y) Z)))
|=============================
|Step 4
|
|? (pp c1318872 c1318871)
|
|1. (~ (ntpp c1318872 c1318871))
|2. (~ (tpp c1318872 c1318871))
|3. (pp c1318872 c1318871)
|
|> hyp
=============================
Step 5

? (~ (ec (f1312496 c1318872 c1318871 Var32) c1318872))

1. (~ (ntpp c1318872 c1318871))
2. (~ (tpp c1318872 c1318871))
3. (pp c1318872 c1318871)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 6
||
||? (pp c1318872 Var36)
||
||1. (ec (f1312496 c1318872 c1318871 Var32) c1318872)
||2. (~ (ntpp c1318872 c1318871))
||3. (~ (tpp c1318872 c1318871))
||4. (pp c1318872 c1318871)
||
||> hyp
|=============================
|Step 7
|
|? (ec (f1312496 c1318872 c1318871 Var32) c1318871)
|
|1. (ec (f1312496 c1318872 c1318871 Var32) c1318872)
|2. (~ (ntpp c1318872 c1318871))
|3. (~ (tpp c1318872 c1318871))
|4. (pp c1318872 c1318871)
|
|> ((ec (f1312496 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 8
||
||? (~ (ntpp c1318872 c1318871))
||
||1. (~ (ec (f1312496 c1318872 c1318871 Var32) c1318871))
||2. (ec (f1312496 c1318872 c1318871 Var32) c1318872)
||3. (~ (ntpp c1318872 c1318871))
||4. (~ (tpp c1318872 c1318871))
||5. (pp c1318872 c1318871)
||
||> hyp
|=============================
|Step 9
|
|? (pp c1318872 c1318871)
|
|1. (~ (ec (f1312496 c1318872 c1318871 Var32) c1318871))
|2. (ec (f1312496 c1318872 c1318871 Var32) c1318872)
|3. (~ (ntpp c1318872 c1318871))
|4. (~ (tpp c1318872 c1318871))
|5. (pp c1318872 c1318871)
|
|> hyp
=============================
Step 10

? (~ (tpp c1318872 c1318871))

1. (ec (f1312496 c1318872 c1318871 Var32) c1318872)
2. (~ (ntpp c1318872 c1318871))
3. (~ (tpp c1318872 c1318871))
4. (pp c1318872 c1318871)

> hyp


LEMMA

Use Lemma7. In the dc case finish immediately. In the connected case use Lemma8; then split pp into tpp or ntpp with Lemma9.
=============================
Step 1

? (all x (all y (all z (((tpp x y) & (po y z)) => (((((dc x z) v (ec x z)) v (po x z)) v (tpp x z)) v (ntpp x z))))))


> revsk
=============================
Step 2

? (((~ (tpp c1325512 c1325511)) v (~ (po c1325511 c1325510))) v (((((dc c1325512 c1325510) v (ec c1325512 c1325510)) v (po c1325512 c1325510)) v (tpp c1325512 c1325510)) v (ntpp c1325512 c1325510)))


> hypdisj
=============================
Step 3

? (ntpp c1325512 c1325510)

1. (~ (tpp c1325512 c1325510))
2. (~ (po c1325512 c1325510))
3. (~ (ec c1325512 c1325510))
4. (~ (dc c1325512 c1325510))
5. (po c1325511 c1325510)
6. (tpp c1325512 c1325511)

> ((ntpp X Y) <-- (pp X Y) (~ (tpp X Y)))
|=============================
|Step 4
|
|? (pp c1325512 c1325510)
|
|1. (~ (ntpp c1325512 c1325510))
|2. (~ (tpp c1325512 c1325510))
|3. (~ (po c1325512 c1325510))
|4. (~ (ec c1325512 c1325510))
|5. (~ (dc c1325512 c1325510))
|6. (po c1325511 c1325510)
|7. (tpp c1325512 c1325511)
|
|> ((pp Y Z) <-- (tpp Y X) (po X Z) (c Y Z) (~ (ec Y Z)) (~ (po Y Z)))
|||||=============================
|||||Step 5
|||||
|||||? (tpp c1325512 Var34)
|||||
|||||1. (~ (pp c1325512 c1325510))
|||||2. (~ (ntpp c1325512 c1325510))
|||||3. (~ (tpp c1325512 c1325510))
|||||4. (~ (po c1325512 c1325510))
|||||5. (~ (ec c1325512 c1325510))
|||||6. (~ (dc c1325512 c1325510))
|||||7. (po c1325511 c1325510)
|||||8. (tpp c1325512 c1325511)
|||||
|||||> hyp
||||=============================
||||Step 6
||||
||||? (po c1325511 c1325510)
||||
||||1. (~ (pp c1325512 c1325510))
||||2. (~ (ntpp c1325512 c1325510))
||||3. (~ (tpp c1325512 c1325510))
||||4. (~ (po c1325512 c1325510))
||||5. (~ (ec c1325512 c1325510))
||||6. (~ (dc c1325512 c1325510))
||||7. (po c1325511 c1325510)
||||8. (tpp c1325512 c1325511)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (c c1325512 c1325510)
|||
|||1. (~ (pp c1325512 c1325510))
|||2. (~ (ntpp c1325512 c1325510))
|||3. (~ (tpp c1325512 c1325510))
|||4. (~ (po c1325512 c1325510))
|||5. (~ (ec c1325512 c1325510))
|||6. (~ (dc c1325512 c1325510))
|||7. (po c1325511 c1325510)
|||8. (tpp c1325512 c1325511)
|||
|||> ((c X Y) <-- (~ (dc X Y)))
|||=============================
|||Step 8
|||
|||? (~ (dc c1325512 c1325510))
|||
|||1. (~ (c c1325512 c1325510))
|||2. (~ (pp c1325512 c1325510))
|||3. (~ (ntpp c1325512 c1325510))
|||4. (~ (tpp c1325512 c1325510))
|||5. (~ (po c1325512 c1325510))
|||6. (~ (ec c1325512 c1325510))
|||7. (~ (dc c1325512 c1325510))
|||8. (po c1325511 c1325510)
|||9. (tpp c1325512 c1325511)
|||
|||> hyp
||=============================
||Step 9
||
||? (~ (ec c1325512 c1325510))
||
||1. (~ (pp c1325512 c1325510))
||2. (~ (ntpp c1325512 c1325510))
||3. (~ (tpp c1325512 c1325510))
||4. (~ (po c1325512 c1325510))
||5. (~ (ec c1325512 c1325510))
||6. (~ (dc c1325512 c1325510))
||7. (po c1325511 c1325510)
||8. (tpp c1325512 c1325511)
||
||> hyp
|=============================
|Step 10
|
|? (~ (po c1325512 c1325510))
|
|1. (~ (pp c1325512 c1325510))
|2. (~ (ntpp c1325512 c1325510))
|3. (~ (tpp c1325512 c1325510))
|4. (~ (po c1325512 c1325510))
|5. (~ (ec c1325512 c1325510))
|6. (~ (dc c1325512 c1325510))
|7. (po c1325511 c1325510)
|8. (tpp c1325512 c1325511)
|
|> hyp
=============================
Step 11

? (~ (tpp c1325512 c1325510))

1. (~ (ntpp c1325512 c1325510))
2. (~ (tpp c1325512 c1325510))
3. (~ (po c1325512 c1325510))
4. (~ (ec c1325512 c1325510))
5. (~ (dc c1325512 c1325510))
6. (po c1325511 c1325510)
7. (tpp c1325512 c1325511)

> hyp
